Nuprl Definition : proddeq
0,22
postcript
pdf
proddeq(
a
;
b
)(
p
,
q
) == 1of(
a
)(1of(
p
),1of(
q
))
1of(
b
)(2of(
p
),2of(
q
))
latex
Definitions
x
.
A
(
x
)
,
p
q
,
f
(
a
)
,
1of(
t
)
,
2of(
t
)
FDL editor aliases
proddeq
origin
1of(b)(2of(p),2of(q)) 1of(b)(2of(p),2of(q)) 
x.A(x) q